% !TEX root = eventadapt-wsfm.tex
We now illustrate how 
the buyer-seller scenario discussed in the Introduction 
can be casted in the compartmentalized model given in \S\,\ref{s:arch}. 
Buyer \pt{B} and seller \pt{S} are implemented as two separate applications, named $\mathsf{byr}$  and $\mathsf{slr}$, respectively:
\begin{eqnarray*}
 sys &::=& \myapp{\mathsf{byr}}{R_b}{\mathsf{S_b}}{\mathcal{M}_b} \appar
\myapp{\mathsf{slr}}{R_s}{\mathsf{S_s}}{\mathcal{M}_s} \parallel \mathcal{H}_s\\ 
R_b &::=& \scomponentbig{\locf{buyer}}{  \nopenr{u@\mathsf{slr}}{x:\ST}.P^{50}_x} \\
\mathsf{S_b} &::=& \que{\locf{buyer}}{\epsilon}\\
R_s &::=& \scomponentbig{\locf{seller}}{ \repopen{u}{y{:}\STT}.Q_y}\\
\mathsf{S_s} &::=& \que{\locf{seller}}{\epsilon}
\end{eqnarray*}
Notice that the service offered by \pt{S} is given as a service definition.
Since applications are intended to be distributed containers of communication behavior, we slightly reformulate the adaptation discussed in the Introduction as follows. We will assume that the seller may receive an update request from its environment. Upon reception of such a request, its associated handler $\mathcal{H}_s$ will not only spawn an update process but will also issue an adaptation request for the buyer. From the perspective of the buyer such a request is internal, for it comes from the seller. That is, the seller acts an an intermediate manager for the buyer. As soon as the buyer receives the internal request, its (local) manager $\mathcal{M}_b$ may spawn an update process at the local level. 
More precisely, 
letting $g_s = \arrive{\locf{seller}@{\mathsf{slr}}, \mathtt{upd}_E} $
and $g_b = \arrive{\locf{buyer}, \mathtt{upd}_I}$, % to stand for guards
we have:
%Now handlers and managers are supposed to react to external and internal requests respectively. The adaptation routine described in the Introduction can be thought as a response to an external signal requesting to update the behavior of the whole system. 
%Thus it can be encoded as: 
%$$
%\begin{eqnarray*}
%%
%\mathcal{H} &::=& 
%*\,\ift{\arrive{\locf{seller}@{\mathsf{slr}}, \mathtt{upd}_E} } 
%{\\&& \qquad
%\nadaptbig{\locf{seller}}{\mathsf{case } \ x\  \mathsf{of}
%%\begin{rcases}
%\{ (x{:}\ST)  :  {Q_y},  \quad
%(x{:}\ST^{}_{\mathtt{pay}})  : { Q^*_y}\} 
%%\end{rcases}
%} \parallel
%\\&& \qquad
%\nadaptbig{\locf{buyer}}{\mathsf{case}\ y \  \mathsf{of}
%%\begin{rcases}
%\{ ( y{:}\STT) :  { P^{100}_x}, \quad  
%( y{:}\STT^{}_{\mathtt{pay}})  :{ P^*_x} 
%%\end{rcases}
%}
%}
%\end{eqnarray*}

\begin{eqnarray*}
\mathcal{H}_s & = & *\,\ift{g_s} {{\nadaptbigg{\locf{seller}}{
\mathsf{case\,}y\, \mathsf{of}
\begin{rcases}
(y{:}\STT) & :  Q_y \para   \outC{\locf{buyer}@\mathsf{byr}}{\mathtt{upd}_I}  \\
(y{:}\STT^{}_{\mathtt{pay}}) & :  Q^*_y \para  \outC{\locf{buyer}@\mathsf{byr}}{\mathtt{upd}_I} 
\end{rcases}
}}}
\\
\mathcal{M}_b & = & *\,\ift{g_b}{{\nadaptbigg{\locf{buyer}}{
\mathsf{case\,}x\, \mathsf{of}
\begin{rcases}
(x{:}\ST) & :  P_x^{100}   \\
(x{:}\ST^{}_{\mathtt{pay}}) & :  P^*_x 
\end{rcases}
}}}{} 
\end{eqnarray*}
For simplicity, in $\mathcal{H}_s$ we use the same message $\mathtt{upd}_I$ for both alternatives of the update.
A more flexible specification could be obtained by 
defining different classes of internal messages for the buyer (say, indexed requests $\mathtt{upd}_I^1$ and $\mathtt{upd}_I^2$) 
and then adapting $\mathcal{M}_b$ to react differently depending on the class of the received internal request.

%
%meaning that the handler waits for the arrival of and update signal in both location queues  of $\locf{buyer}$ and  $\locf{seller}$. Once the signal is received the result is an update of both localities.
%
%Internal requests are instead handled by the internal manager $\mathcal{M}$. For instance upon arrival of an update message $\mathtt{upd}_I$ on queue $\locf{seller}$, if (and only in this case) the selling protocol has entered the case of a $\mathtt{payp}$ payment transaction the protocol is updated with a new  implementation for this case $P^{\mathtt{new}}$:
%\begin{eqnarray*}
% \mathcal{M}_s :: = *\,\ift{\arrive{\locf{seller}, \mathtt{upd}_I}}{\nadaptbig{\locf{seller}}{\mathsf{case}\ y \  \mathsf{of} (y:\beta_{\mathtt{pp}}) : P^{\mathtt{new}}  }}
%\end{eqnarray*}

